Search for: All records

Linear temporal logic (LTL) with the knowledge operator, denoted as KLTL, is a variant of LTL that incorporates what an agent knows or learns at run-time into its specification. Therefore it is an appropriate logical formalism to specify tasks for systems with unknown components that are learned or estimated at run-time. In this paper, we consider a linear system whose system matrices are unknown but come from an a priori known finite set. We introduce a form of KLTL that can be interpreted over the trajectories of such systems. Finally, we show how controllers that guarantee satisfaction of specifications given in fragments of this form of KLTL can be synthesized using optimization techniques. Our results are demonstrated in simulation and on hardware in a drone scenario where the task of the drone is conditioned on its health status, which is unknown a priori and discovered at run-time. 

In this paper, we present a compositional condition for ensuring safety of a collection of interacting systems modeled by inter-triggering hybrid automata (ITHA). ITHA is a modeling formalism for representing multi-agent systems in which each agent is governed by individual dynamics but can also interact with other agents through triggering actions. These triggering actions result in a jump/reset in the state of other agents according to a global resolution function. A sufficient condition for safety of the collection, inspired by responsibility-sensitive safety, is developed in two parts: self-safety relating to the individual dynamics, and responsibility relating to the triggering actions. The condition relies on having an over-approximation method for the resolution function. We further show how such over-approximations can be obtained and improved via communication. We use two examples, a job scheduling task on parallel processors and a highway driving example, throughout the paper to illustrate the concepts. Finally, we provide a comprehensive evaluation on how the proposed condition can be leveraged for several multi-agent control and supervision examples. 

This paper presents a new method of controller synthesis for hidden mode switched systems, where the disturbances are the quantities that are affected by the unobserved switches. Rather than using model discrimination techniques that rely on modifying desired control actions to achieve identification, the controller uses consistency sets which map the measured external behaviors to a belief about which mode signal is being executed and a control action. This hybrid controller is a prefix-based controller, where the prefixes come from an offline constructed belief graph that incorporates prior information about switching sequences with potential reachable sets of the dynamics. While the mode signal is hidden to the controller, the system’s location on the belief graph is fully observed and allows for this problem to be transformed into a design problem in which a discrete mode, in terms of beliefs, is directly observed. Finally, it is shown that affine controllers dependent on prefixes of such beliefs can be synthesized via linear programming.